****************************************************************
From group theory

(define group
  {--> symbol}
-> (kb-> 
      [[all x [all y [all z [[+ x [+ y z]] = [+ [+ x y] z]]]]]
       [all x [[+ e x] = x]]
       [all x [[+ x e] =  x]]
       [all x [[+ x [inv x]] = e]]]))
       
(group) 

(<-kb [all a [all x [[[+ a x] = e] => [a = [inv x]]]]])
run time: 0.484375 secs
779429 inferences, equality = true
depth = 8, complexity = 16, timeout = 60 secs
true

****************************************************************
Step 1

? (all a (all x (((+ a x) = e) => (a = (inv x)))))


> revsk
=============================
Step 2

? ((~ ((+ c22737 c22736) = e)) v (c22737 = (inv c22736)))


> hypdisj
=============================
Step 3

? (c22737 = (inv c22736))

1. ((+ c22737 c22736) = e)

> rewriteB c22737
|=============================
|Step 4
|
|? ((+ c22737 e) = c22737)
|
|1. ((+ c22737 c22736) = e)
|
|> (((+ X e) = X) <--)
=============================
Step 5

? ((+ c22737 e) = (inv c22736))

1. ((+ c22737 c22736) = e)

> rewriteB e
|=============================
|Step 6
|
|? ((+ Var76 (inv Var76)) = e)
|
|1. ((+ c22737 c22736) = e)
|
|> (((+ X (inv X)) = e) <--)
=============================
Step 7

? ((+ c22737 (+ c22736 (inv c22736))) = (inv c22736))

1. ((+ c22737 c22736) = e)

> rewriteA (+ c22737 (+ c22736 (inv c22736)))
|=============================
|Step 8
|
|? ((+ c22737 (+ c22736 (inv c22736))) = (+ (+ c22737 c22736) (inv c22736)))
|
|1. ((+ c22737 c22736) = e)
|
|> (((+ X (+ Y Z)) = (+ (+ X Y) Z)) <--)
=============================
Step 9

? ((+ (+ c22737 c22736) (inv c22736)) = (inv c22736))

1. ((+ c22737 c22736) = e)

> rewriteA (+ c22737 c22736)
|=============================
|Step 10
|
|? ((+ c22737 c22736) = Var86)
|
|1. ((+ c22737 c22736) = e)
|
|> hyp
=============================
Step 11

? ((+ e (inv c22736)) = (inv c22736))

1. ((+ c22737 c22736) = e)

> (((+ e X) = X) <--)
